COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(declare (special refuted d c p n) (fixsw t))
C00007 ENDMK
C⊗;
(declare (special refuted d c p n) (fixsw t))

(defun implies (premise conclusion)
       (add-conjunction premise (opposite conclusion) () () () ()))

(defun opposite (f)
 (caseq (car f)
	(AND
	 `(or ,(opposite (cadr f)) . ,(opposite (cddr f))))
	(OR 
	 `(and  ,(opposite (cadr f)) . ,(opposite (cddr f))))
	(+
	 `(- . ,(cdr f)))
	(-
	 `(+ . ,(cdr f)))
	(t ())))

(defun add-conjunction (f g d c p n)
 (let ((refuted ()))
      (expand f)
      (expand g)
      (cond 
       (refuted t)
       ((not (atom d))
	(split (cadr (car d))
	       (cddr (car d))
	       (cdr d)))
       (t ()))))

(defun split (f1 g1 d)
       (let ((f (opposite f1))
	     (g (opposite g1)))
	    (and (add-conjunction f  g1 d c p n)
		 (add-conjunction f  g  d c p n)
		 (add-conjunction f1 g  d c p n))))

(defun expand (f)
 (caseq (car f)
	(AND 
	 (cond ((member f d)
		(setq refuted t))
	       ((member f c))
	       (t (setq c `(,f . ,c))
		  (expand (cadr f))
		  (expand (cddr f)))))
	(OR 
	 (setq d (extend (opposite f) d c)))
	(+
	 (setq p (extend (cdr f) p n)))
	(-
	 (setq n (extend (cdr f) n p))) 
	(t ()))
 ())

(defun extend (f a b)
       (cond ((member f b)
	      (setq refuted t) a)
	     ((member f a) a)
	     (t `(,f . ,a))))

(defmacro try (p c  m)
 `(do ((i ,(// m 10.) (1- i)))
      ((= i 0) t)
      (implies ,p ,c)
      (implies ,p ,c)
      (implies ,p ,c)
      (implies ,p ,c)
      (implies ,p ,c)
      (implies ,p ,c)
      (implies ,p ,c)
      (implies ,p ,c)
      (implies ,p ,c)
      (implies ,p ,c)))

(include "timer.lsp")
(timer timit
       (progn 
	(try '(- . a) '(+ . a) 1000.)
	(try  '(+ . b) '(or (- . b) . (- . b)) 1000.)
	(try '(+ . nothing) '(or (+ . to-be) . (- . to-be)) 1000.)
	(try '(or (- . a) . (- . a)) '(- . a) 1000.)
	(try '(- . b) '(or (+ . a) . (- . b)) 1000.)
	(try '(and (- . a) . (- . b))
	       '(and (- . b) . (- . a)) 1000.)
	(try '(- . b) '(or (- . a) . (and (+ . a) . (- . b))) 1000.)
	(try '(or (- . a) . (or (- . b) . (+ . c)))
	     '(or (- . b) . (or (- . a) . (+ . c))) 1000.)
	(try '(or ( - . a) . (+ . b))
	     '(or (and (+ . b) . (- . c))
				   . (or (- . a) . (+ . c))) 1000.)
	(try '(and (or (- . a) . ( + . c)).
		   (or (- . b) . (+ . c)))
	     '(or (and (- . a) . (- . b)) . (+ . c)) 1000.)))